Left Termination of the query pattern
conf(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 188 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 174 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 8 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPOrderProof (⇔, 155 ms)
        ↳27 QDP
        ↳28 DependencyGraphProof (⇔, 0 ms)
        ↳29 TRUE
    ↳30 PiDP
        ↳31 UsableRulesProof (⇔, 0 ms)
        ↳32 PiDP
        ↳33 PiDPToQDPProof (⇒, 0 ms)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔, 0 ms)
        ↳36 YES
    ↳37 PiDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 PiDP
        ↳40 PiDPToQDPProof (⇒, 0 ms)
        ↳41 QDP
        ↳42 QDPSizeChangeProof (⇔, 0 ms)
        ↳43 YES

(0) Obligation:

Clauses:

conf(X) :- ','(del2(X, Z), ','(del(U, Y, Z), conf(Y))).
del2(X, Y) :- ','(del(U, X, Z), del(V, Z, Y)).
del(X, .(X, T), T).
del(X, .(H, T), .(H, T1)) :- del(X, T, T1).
s2l(s(X), .(Y, Xs)) :- s2l(X, Xs).
s2l(0, []).
goal(X) :- ','(s2l(X, XS), conf(XS)).

Query: conf(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

delA(X1, .(X2, X3), .(X2, X4)) :- delA(X1, X3, X4).
delB(X1, .(X2, X3), .(X2, X4)) :- delB(X1, X3, X4).
delC(X1, .(X2, X3), .(X2, X4)) :- delC(X1, X3, X4).
confD(X1) :- delC(X2, X1, X3).
confD(X1) :- ','(delcC(X2, X1, X3), delC(X4, X3, X5)).
confD(X1) :- ','(del2cE(X1, X2), delF(X3, X4, X2)).
confD(X1) :- ','(del2cE(X1, X2), ','(delcF(X3, X4, X2), confD(X4))).
delF(X1, .(X2, X3), .(X2, X4)) :- delF(X1, X3, X4).
confG(X1) :- delA(X2, X1, X3).
confG(X1) :- ','(delcA(X2, X1, X3), delA(X4, X3, X5)).
confG(X1) :- ','(delcA(X2, X1, X3), ','(delcA(X4, X3, X5), delB(X6, X7, X5))).
confG(X1) :- ','(delcA(X2, X1, X3), ','(delcA(X4, X3, X5), ','(delcB(X6, X7, X5), confD(X7)))).

Clauses:

delcA(X1, .(X1, X2), X2).
delcA(X1, .(X2, X3), .(X2, X4)) :- delcA(X1, X3, X4).
delcB(X1, .(X1, X2), X2).
delcB(X1, .(X2, X3), .(X2, X4)) :- delcB(X1, X3, X4).
delcC(X1, .(X1, X2), X2).
delcC(X1, .(X2, X3), .(X2, X4)) :- delcC(X1, X3, X4).
confcD(X1) :- ','(del2cE(X1, X2), ','(delcF(X3, X4, X2), confcD(X4))).
delcF(X1, .(X1, X2), X2).
delcF(X1, .(X2, X3), .(X2, X4)) :- delcF(X1, X3, X4).
del2cE(X1, X2) :- ','(delcC(X3, X1, X4), delcC(X5, X4, X2)).

Afs:

confG(x1)  =  confG(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
confG_in: (b)
delA_in: (f,b,f)
delcA_in: (f,b,f)
delB_in: (f,f,b)
delcB_in: (f,f,b)
confD_in: (b)
delC_in: (f,b,f)
delcC_in: (f,b,f)
del2cE_in: (b,f)
delF_in: (f,f,b)
delcF_in: (f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

CONFG_IN_G(X1) → U12_G(X1, delA_in_aga(X2, X1, X3))
CONFG_IN_G(X1) → DELA_IN_AGA(X2, X1, X3)
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, delA_in_aga(X1, X3, X4))
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)
CONFG_IN_G(X1) → U13_G(X1, delcA_in_aga(X2, X1, X3))
U13_G(X1, delcA_out_aga(X2, X1, X3)) → U14_G(X1, delA_in_aga(X4, X3, X5))
U13_G(X1, delcA_out_aga(X2, X1, X3)) → DELA_IN_AGA(X4, X3, X5)
U13_G(X1, delcA_out_aga(X2, X1, X3)) → U15_G(X1, delcA_in_aga(X4, X3, X5))
U15_G(X1, delcA_out_aga(X4, X3, X5)) → U16_G(X1, delB_in_aag(X6, X7, X5))
U15_G(X1, delcA_out_aga(X4, X3, X5)) → DELB_IN_AAG(X6, X7, X5)
DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → U2_AAG(X1, X2, X3, X4, delB_in_aag(X1, X3, X4))
DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELB_IN_AAG(X1, X3, X4)
U15_G(X1, delcA_out_aga(X4, X3, X5)) → U17_G(X1, delcB_in_aag(X6, X7, X5))
U17_G(X1, delcB_out_aag(X6, X7, X5)) → U18_G(X1, confD_in_g(X7))
U17_G(X1, delcB_out_aag(X6, X7, X5)) → CONFD_IN_G(X7)
CONFD_IN_G(X1) → U4_G(X1, delC_in_aga(X2, X1, X3))
CONFD_IN_G(X1) → DELC_IN_AGA(X2, X1, X3)
DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U3_AGA(X1, X2, X3, X4, delC_in_aga(X1, X3, X4))
DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELC_IN_AGA(X1, X3, X4)
CONFD_IN_G(X1) → U5_G(X1, delcC_in_aga(X2, X1, X3))
U5_G(X1, delcC_out_aga(X2, X1, X3)) → U6_G(X1, delC_in_aga(X4, X3, X5))
U5_G(X1, delcC_out_aga(X2, X1, X3)) → DELC_IN_AGA(X4, X3, X5)
CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → U8_G(X1, delF_in_aag(X3, X4, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → DELF_IN_AAG(X3, X4, X2)
DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → U11_AAG(X1, X2, X3, X4, delF_in_aag(X1, X3, X4))
DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELF_IN_AAG(X1, X3, X4)
U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X3, X4, X2))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → U10_G(X1, confD_in_g(X4))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
delA_in_aga(x1, x2, x3)  =  delA_in_aga(x2)
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delB_in_aag(x1, x2, x3)  =  delB_in_aag(x3)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
confD_in_g(x1)  =  confD_in_g(x1)
delC_in_aga(x1, x2, x3)  =  delC_in_aga(x2)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delF_in_aag(x1, x2, x3)  =  delF_in_aag(x3)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
CONFG_IN_G(x1)  =  CONFG_IN_G(x1)
U12_G(x1, x2)  =  U12_G(x1, x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x3, x5)
U13_G(x1, x2)  =  U13_G(x1, x2)
U14_G(x1, x2)  =  U14_G(x1, x2)
U15_G(x1, x2)  =  U15_G(x1, x2)
U16_G(x1, x2)  =  U16_G(x1, x2)
DELB_IN_AAG(x1, x2, x3)  =  DELB_IN_AAG(x3)
U2_AAG(x1, x2, x3, x4, x5)  =  U2_AAG(x4, x5)
U17_G(x1, x2)  =  U17_G(x1, x2)
U18_G(x1, x2)  =  U18_G(x1, x2)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
DELC_IN_AGA(x1, x2, x3)  =  DELC_IN_AGA(x2)
U3_AGA(x1, x2, x3, x4, x5)  =  U3_AGA(x3, x5)
U5_G(x1, x2)  =  U5_G(x1, x2)
U6_G(x1, x2)  =  U6_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)
U8_G(x1, x2)  =  U8_G(x1, x2)
DELF_IN_AAG(x1, x2, x3)  =  DELF_IN_AAG(x3)
U11_AAG(x1, x2, x3, x4, x5)  =  U11_AAG(x4, x5)
U9_G(x1, x2)  =  U9_G(x1, x2)
U10_G(x1, x2)  =  U10_G(x1, x2)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CONFG_IN_G(X1) → U12_G(X1, delA_in_aga(X2, X1, X3))
CONFG_IN_G(X1) → DELA_IN_AGA(X2, X1, X3)
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, delA_in_aga(X1, X3, X4))
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)
CONFG_IN_G(X1) → U13_G(X1, delcA_in_aga(X2, X1, X3))
U13_G(X1, delcA_out_aga(X2, X1, X3)) → U14_G(X1, delA_in_aga(X4, X3, X5))
U13_G(X1, delcA_out_aga(X2, X1, X3)) → DELA_IN_AGA(X4, X3, X5)
U13_G(X1, delcA_out_aga(X2, X1, X3)) → U15_G(X1, delcA_in_aga(X4, X3, X5))
U15_G(X1, delcA_out_aga(X4, X3, X5)) → U16_G(X1, delB_in_aag(X6, X7, X5))
U15_G(X1, delcA_out_aga(X4, X3, X5)) → DELB_IN_AAG(X6, X7, X5)
DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → U2_AAG(X1, X2, X3, X4, delB_in_aag(X1, X3, X4))
DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELB_IN_AAG(X1, X3, X4)
U15_G(X1, delcA_out_aga(X4, X3, X5)) → U17_G(X1, delcB_in_aag(X6, X7, X5))
U17_G(X1, delcB_out_aag(X6, X7, X5)) → U18_G(X1, confD_in_g(X7))
U17_G(X1, delcB_out_aag(X6, X7, X5)) → CONFD_IN_G(X7)
CONFD_IN_G(X1) → U4_G(X1, delC_in_aga(X2, X1, X3))
CONFD_IN_G(X1) → DELC_IN_AGA(X2, X1, X3)
DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U3_AGA(X1, X2, X3, X4, delC_in_aga(X1, X3, X4))
DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELC_IN_AGA(X1, X3, X4)
CONFD_IN_G(X1) → U5_G(X1, delcC_in_aga(X2, X1, X3))
U5_G(X1, delcC_out_aga(X2, X1, X3)) → U6_G(X1, delC_in_aga(X4, X3, X5))
U5_G(X1, delcC_out_aga(X2, X1, X3)) → DELC_IN_AGA(X4, X3, X5)
CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → U8_G(X1, delF_in_aag(X3, X4, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → DELF_IN_AAG(X3, X4, X2)
DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → U11_AAG(X1, X2, X3, X4, delF_in_aag(X1, X3, X4))
DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELF_IN_AAG(X1, X3, X4)
U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X3, X4, X2))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → U10_G(X1, confD_in_g(X4))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
delA_in_aga(x1, x2, x3)  =  delA_in_aga(x2)
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delB_in_aag(x1, x2, x3)  =  delB_in_aag(x3)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
confD_in_g(x1)  =  confD_in_g(x1)
delC_in_aga(x1, x2, x3)  =  delC_in_aga(x2)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delF_in_aag(x1, x2, x3)  =  delF_in_aag(x3)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
CONFG_IN_G(x1)  =  CONFG_IN_G(x1)
U12_G(x1, x2)  =  U12_G(x1, x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x3, x5)
U13_G(x1, x2)  =  U13_G(x1, x2)
U14_G(x1, x2)  =  U14_G(x1, x2)
U15_G(x1, x2)  =  U15_G(x1, x2)
U16_G(x1, x2)  =  U16_G(x1, x2)
DELB_IN_AAG(x1, x2, x3)  =  DELB_IN_AAG(x3)
U2_AAG(x1, x2, x3, x4, x5)  =  U2_AAG(x4, x5)
U17_G(x1, x2)  =  U17_G(x1, x2)
U18_G(x1, x2)  =  U18_G(x1, x2)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
DELC_IN_AGA(x1, x2, x3)  =  DELC_IN_AGA(x2)
U3_AGA(x1, x2, x3, x4, x5)  =  U3_AGA(x3, x5)
U5_G(x1, x2)  =  U5_G(x1, x2)
U6_G(x1, x2)  =  U6_G(x1, x2)
U7_G(x1, x2)  =  U7_G(x1, x2)
U8_G(x1, x2)  =  U8_G(x1, x2)
DELF_IN_AAG(x1, x2, x3)  =  DELF_IN_AAG(x3)
U11_AAG(x1, x2, x3, x4, x5)  =  U11_AAG(x4, x5)
U9_G(x1, x2)  =  U9_G(x1, x2)
U10_G(x1, x2)  =  U10_G(x1, x2)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 23 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELF_IN_AAG(X1, X3, X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
DELF_IN_AAG(x1, x2, x3)  =  DELF_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELF_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELF_IN_AAG(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELF_IN_AAG(x1, x2, x3)  =  DELF_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELF_IN_AAG(.(X4)) → DELF_IN_AAG(X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELF_IN_AAG(.(X4)) → DELF_IN_AAG(X4)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELC_IN_AGA(X1, X3, X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
DELC_IN_AGA(x1, x2, x3)  =  DELC_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELC_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELC_IN_AGA(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELC_IN_AGA(x1, x2, x3)  =  DELC_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELC_IN_AGA(.(X3)) → DELC_IN_AGA(X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELC_IN_AGA(.(X3)) → DELC_IN_AGA(X3)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X3, X4, X2))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U7_G(x1, x2)  =  U7_G(x1, x2)
U9_G(x1, x2)  =  U9_G(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1, X2))
U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X3, X4, X2))
U9_G(X1, delcF_out_aag(X3, X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U7_G(x1, x2)  =  U7_G(x1, x2)
U9_G(x1, x2)  =  U9_G(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1))
U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X2))
U9_G(X1, delcF_out_aag(X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

del2cE_in_ga(X1) → U27_ga(X1, delcC_in_aga(X1))
delcF_in_aag(X2) → delcF_out_aag(.(X2), X2)
delcF_in_aag(.(X4)) → U26_aag(X4, delcF_in_aag(X4))
U27_ga(X1, delcC_out_aga(X1, X4)) → U28_ga(X1, delcC_in_aga(X4))
U26_aag(X4, delcF_out_aag(X3, X4)) → delcF_out_aag(.(X3), .(X4))
delcC_in_aga(.(X2)) → delcC_out_aga(.(X2), X2)
delcC_in_aga(.(X3)) → U22_aga(X3, delcC_in_aga(X3))
U28_ga(X1, delcC_out_aga(X4, X2)) → del2cE_out_ga(X1, X2)
U22_aga(X3, delcC_out_aga(X3, X4)) → delcC_out_aga(.(X3), .(X4))

The set Q consists of the following terms:

del2cE_in_ga(x0)
delcF_in_aag(x0)
U27_ga(x0, x1)
U26_aag(x0, x1)
delcC_in_aga(x0)
U28_ga(x0, x1)
U22_aga(x0, x1)

We have to consider all (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U7_G(X1, del2cE_out_ga(X1, X2)) → U9_G(X1, delcF_in_aag(X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U7_G(x1, x2) ) = 2x2 + 2


POL( del2cE_in_ga(x1) ) = x1


POL( U27_ga(x1, x2) ) = max{0, x2 - 2}


POL( delcC_in_aga(x1) ) = x1 + 1


POL( U9_G(x1, x2) ) = 2x2 + 2


POL( delcF_in_aag(x1) ) = 2x1 + 1


POL( delcF_out_aag(x1, x2) ) = x1


POL( .(x1) ) = 2x1 + 1


POL( U26_aag(x1, x2) ) = 2x2 + 1


POL( U28_ga(x1, x2) ) = max{0, 2x2 - 2}


POL( delcC_out_aga(x1, x2) ) = 2x2 + 2


POL( U22_aga(x1, x2) ) = 2x2


POL( del2cE_out_ga(x1, x2) ) = 2x2 + 2


POL( CONFD_IN_G(x1) ) = 2x1 + 2



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

del2cE_in_ga(X1) → U27_ga(X1, delcC_in_aga(X1))
delcF_in_aag(X2) → delcF_out_aag(.(X2), X2)
delcF_in_aag(.(X4)) → U26_aag(X4, delcF_in_aag(X4))
delcC_in_aga(.(X2)) → delcC_out_aga(.(X2), X2)
delcC_in_aga(.(X3)) → U22_aga(X3, delcC_in_aga(X3))
U27_ga(X1, delcC_out_aga(X1, X4)) → U28_ga(X1, delcC_in_aga(X4))
U26_aag(X4, delcF_out_aag(X3, X4)) → delcF_out_aag(.(X3), .(X4))
U28_ga(X1, delcC_out_aga(X4, X2)) → del2cE_out_ga(X1, X2)
U22_aga(X3, delcC_out_aga(X3, X4)) → delcC_out_aga(.(X3), .(X4))

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONFD_IN_G(X1) → U7_G(X1, del2cE_in_ga(X1))
U9_G(X1, delcF_out_aag(X4, X2)) → CONFD_IN_G(X4)

The TRS R consists of the following rules:

del2cE_in_ga(X1) → U27_ga(X1, delcC_in_aga(X1))
delcF_in_aag(X2) → delcF_out_aag(.(X2), X2)
delcF_in_aag(.(X4)) → U26_aag(X4, delcF_in_aag(X4))
U27_ga(X1, delcC_out_aga(X1, X4)) → U28_ga(X1, delcC_in_aga(X4))
U26_aag(X4, delcF_out_aag(X3, X4)) → delcF_out_aag(.(X3), .(X4))
delcC_in_aga(.(X2)) → delcC_out_aga(.(X2), X2)
delcC_in_aga(.(X3)) → U22_aga(X3, delcC_in_aga(X3))
U28_ga(X1, delcC_out_aga(X4, X2)) → del2cE_out_ga(X1, X2)
U22_aga(X3, delcC_out_aga(X3, X4)) → delcC_out_aga(.(X3), .(X4))

The set Q consists of the following terms:

del2cE_in_ga(x0)
delcF_in_aag(x0)
U27_ga(x0, x1)
U26_aag(x0, x1)
delcC_in_aga(x0)
U28_ga(x0, x1)
U22_aga(x0, x1)

We have to consider all (P,Q,R)-chains.

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(29) TRUE

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELB_IN_AAG(X1, X3, X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
DELB_IN_AAG(x1, x2, x3)  =  DELB_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELB_IN_AAG(X1, .(X2, X3), .(X2, X4)) → DELB_IN_AAG(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELB_IN_AAG(x1, x2, x3)  =  DELB_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELB_IN_AAG(.(X4)) → DELB_IN_AAG(X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELB_IN_AAG(.(X4)) → DELB_IN_AAG(X4)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)

The TRS R consists of the following rules:

delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U20_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U20_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))
delcB_in_aag(X1, .(X1, X2), X2) → delcB_out_aag(X1, .(X1, X2), X2)
delcB_in_aag(X1, .(X2, X3), .(X2, X4)) → U21_aag(X1, X2, X3, X4, delcB_in_aag(X1, X3, X4))
U21_aag(X1, X2, X3, X4, delcB_out_aag(X1, X3, X4)) → delcB_out_aag(X1, .(X2, X3), .(X2, X4))
delcC_in_aga(X1, .(X1, X2), X2) → delcC_out_aga(X1, .(X1, X2), X2)
delcC_in_aga(X1, .(X2, X3), .(X2, X4)) → U22_aga(X1, X2, X3, X4, delcC_in_aga(X1, X3, X4))
U22_aga(X1, X2, X3, X4, delcC_out_aga(X1, X3, X4)) → delcC_out_aga(X1, .(X2, X3), .(X2, X4))
del2cE_in_ga(X1, X2) → U27_ga(X1, X2, delcC_in_aga(X3, X1, X4))
U27_ga(X1, X2, delcC_out_aga(X3, X1, X4)) → U28_ga(X1, X2, delcC_in_aga(X5, X4, X2))
U28_ga(X1, X2, delcC_out_aga(X5, X4, X2)) → del2cE_out_ga(X1, X2)
delcF_in_aag(X1, .(X1, X2), X2) → delcF_out_aag(X1, .(X1, X2), X2)
delcF_in_aag(X1, .(X2, X3), .(X2, X4)) → U26_aag(X1, X2, X3, X4, delcF_in_aag(X1, X3, X4))
U26_aag(X1, X2, X3, X4, delcF_out_aag(X1, X3, X4)) → delcF_out_aag(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U20_aga(x1, x2, x3, x4, x5)  =  U20_aga(x3, x5)
delcB_in_aag(x1, x2, x3)  =  delcB_in_aag(x3)
delcB_out_aag(x1, x2, x3)  =  delcB_out_aag(x2, x3)
U21_aag(x1, x2, x3, x4, x5)  =  U21_aag(x4, x5)
delcC_in_aga(x1, x2, x3)  =  delcC_in_aga(x2)
delcC_out_aga(x1, x2, x3)  =  delcC_out_aga(x2, x3)
U22_aga(x1, x2, x3, x4, x5)  =  U22_aga(x3, x5)
del2cE_in_ga(x1, x2)  =  del2cE_in_ga(x1)
U27_ga(x1, x2, x3)  =  U27_ga(x1, x3)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
del2cE_out_ga(x1, x2)  =  del2cE_out_ga(x1, x2)
delcF_in_aag(x1, x2, x3)  =  delcF_in_aag(x3)
delcF_out_aag(x1, x2, x3)  =  delcF_out_aag(x2, x3)
U26_aag(x1, x2, x3, x4, x5)  =  U26_aag(x4, x5)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(.(X3)) → DELA_IN_AGA(X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELA_IN_AGA(.(X3)) → DELA_IN_AGA(X3)
    The graph contains the following edges 1 > 1

(43) YES